Nuprl Lemma : sorted-merge
11,40
postcript
pdf
T
:Type. subtype_rel(
T
;
)
(
bs
,
as
:(
T
List). sorted(
as
)
sorted(merge(
as
;
bs
)))
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
sorted(
L
)
,
merge(
as
;
bs
)
,
subtype(
S
;
T
)
Lemmas
sorted
wf
,
s-insert-sorted
,
merge
wf
origin
T:Type. subtype_rel(T; 
) 
(bs,as:(T List). sorted(as) sorted(merge(as; bs))) T:Type. subtype_rel(T; ) (bs,as:(T List). sorted(as) sorted(merge(as; bs))) 
T Qx:A. B(x)